A presentation on monitoring cyber-physical systems (CPS) using specification-based approaches to ensure systems meet predefined criteria under varying conditions.
Presented by: Shishir Panta
For class EE/CSC 7700 ML for CPS
Instructor: Dr. Xugui Zhou
A presentation on monitoring cyber-physical systems (CPS) using specification-based approaches to ensure systems meet predefined criteria under varying conditions.
Explains CPS as a combination of computational and physical processes, and specification-based monitoring as a formal, rule-driven approach contrasting with anomaly-based methods.
Monitoring evaluates temporal behaviors in CPS to detect anomalies or failures by comparing system outputs to predefined criteria.
Highlights real-time monitoring during execution and the use of model-based design to simulate and validate system behaviors.
Emphasizes the need for rigorous specification formalisms using temporal logic for verifying CPS behaviors over time.
Introduces Linear-Time Temporal Logic (LTL) for expressing temporal system behaviors with operators like "always" and "eventually."
Details LTL's syntax, including atomic propositions, logical operators, and temporal operators for discrete-event systems.
Compares LTL with regular expressions, noting LTL's focus on temporal relationships and its translation to regular expressions for simpler representations.
Explains CPS monitoring's dual challenges of handling discrete and continuous behaviors, leading to the introduction of Signal Temporal Logic (STL).
STL extends LTL for real-time monitoring of continuous signals, with applications in diverse fields like robotics and biomedical systems.
STL specifies properties of continuous signals using time-bounded operators and numeric predicates for real-time systems.
Illustrates STL's application to real-world systems like autonomous vehicles and temperature control using numerical predicates and temporal operators.
STL handles continuous signals with numeric predicates and quantitative semantics, while LTL focuses on discrete computational systems.
Adapts STL to finite signals by redefining temporal operators like "always" and "eventually" for practical monitoring.
Proposes modifications to STL temporal operators for finite signals, addressing challenges with real-world monitoring.
Explains strict interpretations of operators in continuous-time systems to enhance expressiveness in STL.
Introduces robustness metrics to measure how well a signal satisfies or violates an STL specification.
Describes robustness degree as a quantitative measure of signal compliance with specifications, useful for hybrid systems.
Details LTL's syntax, including atomic propositions, logical operators, and temporal operators for discrete-event systems.
Compares LTL with regular expressions, noting LTL's focus on temporal relationships and its translation to regular expressions for simpler representations.
Explains CPS monitoring's dual challenges of handling discrete and continuous behaviors, leading to the introduction of Signal Temporal Logic (STL).
STL extends LTL for real-time monitoring of continuous signals, with applications in diverse fields like robotics and biomedical systems.
STL specifies properties of continuous signals using time-bounded operators and numeric predicates for real-time systems.
Illustrates STL's application to real-world systems like autonomous vehicles and temperature control using numerical predicates and temporal operators.
STL handles continuous signals with numeric predicates and quantitative semantics, while LTL focuses on discrete computational systems.
Adapts STL to finite signals by redefining temporal operators like "always" and "eventually" for practical monitoring.
Proposes modifications to STL temporal operators for finite signals, addressing challenges with real-world monitoring.
Explains strict interpretations of operators in continuous-time systems to enhance expressiveness in STL.
Introduces robustness metrics to measure how well a signal satisfies or violates an STL specification.
Describes robustness degree as a quantitative measure of signal compliance with specifications, useful for hybrid systems.
Demonstrates STL's robustness degree in practical scenarios, providing quantitative insights into system behavior.
Defines robustness degree mathematically and outlines its application to STL's logical and temporal operators.
Highlights robustness properties, including tolerance to small deviations and its implications for CPS monitoring.
Describes STL monitoring algorithms to verify signal compliance with specifications, focusing on efficiency.
Discusses analyzing entire signal traces post-execution using STL, with linear-time complexity algorithms.
Demonstrates STL's robustness degree in practical scenarios, providing quantitative insights into system behavior.
Defines robustness degree mathematically and outlines its application to STL's logical and temporal operators.
Highlights robustness properties, including tolerance to small deviations and its implications for CPS monitoring.
Describes STL monitoring algorithms to verify signal compliance with specifications, focusing on efficiency.
Discusses analyzing entire signal traces post-execution using STL, with linear-time complexity algorithms.
Explains recursive algorithms for offline STL monitoring, evaluating signals against complex temporal formulas.
Details how satisfaction of STL formulas is computed for various operators and predicates during offline monitoring.
Introduces ComputeSatisfaction functions to evaluate STL formula satisfaction or violation qualitatively and quantitatively.
Online monitoring evaluates partial signals in real-time to determine STL formula satisfaction incrementally.
Proposes three-valued and four-valued semantics for online monitoring to address uncertainty in partial signals.
Quantitative online monitoring algorithms measure signal compliance or violations in real-time using robustness degrees.
Discusses robustness intervals and forecast handling in quantitative online monitoring algorithms.
Introduces horizon and history concepts to manage STL formulas with past and future operators in real-time.
STL-* adds freezing operators to capture dynamic oscillatory behaviors in CPS, improving expressiveness but increasing complexity.
Time-frequency analysis tools like TFL complement STL to monitor complex oscillatory patterns in CPS.
Extensions like SSTL and STREL enable STL to monitor spatial and temporal behaviors in distributed systems like smart grids.
Combines STL with regular expressions to monitor global and local temporal patterns in CPS.
Outlines practical challenges in CPS monitoring, including noisy data, resource limits, and bridging physical-digital systems.
Discusses efficient STL implementation in real-time CPS using discrete-time signals and FPGA-based monitors.
Introduces falsification and parameter synthesis as complementary techniques to test and validate CPS designs.
STL-based tools detect unexpected behaviors in automotive systems like powertrains and autonomous vehicle components.
STL monitors critical properties of artificial pancreas devices, ensuring safety under variable conditions.
Highlights STL's role in medical device monitoring to ensure real-time correctness and reliability.
Discusses STL's applications in real-time health devices like pacemakers and ventilators, emphasizing error minimization.
Summarizes STL's role in CPS monitoring, highlighting advancements in algorithms, semantics, and applications across industries.
Questions STL's coexistence with machine learning in CPS monitoring, emphasizing risks and challenges in defining specifications for complex systems.